COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.device  xgp
C00007 ENDMK
C⊗;
.device  xgp
.FONT 1 "baxl30";		<<normal font>>
.FONT 2 "BAXB30";		<<headings>>
.begin double space; select 2
.group  skip 2
.once center
Automatic Program Generation from Logic Specifications 
.group skip 2;select 1
It has been observed that an algorithm consists of two separable components:
logic and control.  The description of an algorithm, specifying its
logic and control components, can be 
programming-language-independent.  We have designed and implemented
a system that accepts logic specifications, generates algorithms in an
intermediate language, and then translates these algorithms into programs
in specific target languages.

This system is unique in its ability to generate programs in more than
one language.  Moreover, it represents a large non-trivial application of
formal techniques. Many programs of varying sizes have been specified and
generated by the system, the largest being the system itself.

In section I we explain the rationale for approaching the problem of obtaining
correct programs as we have, from logic specifications to equivalent
program. Section II describes the specification language informally, a formal
treatment being available elsewhere. In sections III and IV we show how a
specification is mapped into a deterministic algorithm, and outline the proof
that the algorithm generated satisfies the specification. Section V contains
conclusions that can be drawn from this effort, as well as directions for 
continuing research.
.group skip 4
.begin center
Ruth E. Davis
EECS Department
University of Santa Clara
Santa Clara, CA 95053
.end

.end